/*
	2025-8-11 18:45:03
	from langhat 
*/
#include<iostream>
#include<stdlib.h>
#include<algorithm>
#include<sstream>
#include<map>
#include<set>
#include<vector>
using namespace std;
bool torun=1;
string in,t1,t2;
int mod;//0 ->match md 1 ->all mod 2 ->short mod
set<vector<string>> known;
map<vector<string>,pair<vector<vector<string>>,bool>> rule;
set<string> thing;
/*ai part */
bool isVariable(const string &s) {
    if (s.empty()) return false;
    return (s[0] >= 'A' && s[0] <= 'Z') || (s[0] == '$');
}
bool matchFact(const vector<string> &queryPattern, const vector<string> &fact, map<string, string> &varMap) {
    if (queryPattern.size() != fact.size()) return false;
    for (int i = 0; i < queryPattern.size(); ++i) {
        const string &q = queryPattern[i];
        const string &f = fact[i];

        if (isVariable(q)) {
            if (varMap.find(q) == varMap.end()) {
                varMap[q] = f;
            } else {
                if (varMap[q] != f) {
                    return false;
                }
            }
        } else {
            if (q != f) {
                return false;
            }
        }
    }
    return true;
}
/*end of ai part*/
int main(){
	cout<<"Rethink-β REPL\n(c) 2025 langhat\ninput `exit` to quit.";
	while(torun){
		cout<<"\nRethink:> ";
		getline(cin,in);
		if(in.empty())continue;
		bool ir=0;
		stringstream ss(in);ss>>t1;
		if(t1=="exit"){
			cout<<"Exited.\n";
			torun=0;
			continue;
		}else if(t1=="if"||t1=="ask"){//now didn't use var
			bool hv=0;
			{stringstream ss(in);
			while(ss>>t1){
				if((t1[0]>='A'&&t1[0]<='Z')||t1[0]=='$'){
					hv=1;
				}
			}}
			if(hv){
				stringstream ss(in);
		        ss >> t1;
		        vector<string> queryPattern;
		        while(ss>>t1){
		            queryPattern.push_back(t1);
		        }
		        if(queryPattern.empty()){
		            cout<<"Failed: empty query.\n";
		            continue;
		        }
		        vector<vector<string>> matches;
		        for(auto &fact : known){
		        	map<string, string> varMap; 
		            if(matchFact(queryPattern, fact,varMap)){
		                matches.push_back(fact);
		            }
		        }
		        if(matches.empty()){
		            cout<<"False.\n";
		        }else{
		            cout<<"True. Matches found ("<<matches.size()<<"):\n";
		            for(auto &match : matches){
		                for(int i=0; i<match.size(); ++i){
		                    // 显示变量对应的值（查询模式中是变量的位置，标注变量名）
		                    if(isVariable(queryPattern[i])){
		                    	if(mod==0)
		                        cout<<"["<<queryPattern[i]<<"="<<match[i]<<"] ";
		                        else
		                        cout<<match[i]<<" ";
		                    }else{
		                    	if(mod==1)
		                        cout<<match[i]<<" ";
		                    }
		                }
		                cout<<"\b\n"; // 去掉末尾空格
		            }
		        }
				continue;
			}
			{
			stringstream ss(in);
			ss>>t1;
			vector<string> vs;
			while(ss>>t1){
				vs.push_back(t1);
			}
			if(known.find(vs)!=known.end()){
				cout<<"True.\n";
			}else{
				cout<<"False.\n";
			}
			}
			continue;
		}else if(t1=="erase"){
	        stringstream ss(in);
	        ss >> t1;
	        vector<string> erasePattern;
	        while(ss >> t1){
	            erasePattern.push_back(t1);
	        }
	        if(erasePattern.empty()){
	            cout<<"Failed: empty erase pattern.\n";
	            continue;
	        }
	        vector<vector<string>> toErase;
	        for(auto &fact : known){
	        	map<string, string> varMap; 
	            if(matchFact(erasePattern, fact,varMap)){ 
	                toErase.push_back(fact);
	            }
	        }
	        if(toErase.empty()){
	            cout<<"Failed: no matching facts to erase.\n";
	        }else{
	            for(auto &fact : toErase){
	                known.erase(fact);
	            }
	            cout<<"Ok.";
	            if(mod!=2)cout<<" Erased "<<toErase.size()<<" matching fact(s):\n";
	            for(auto &fact : toErase){
	                for(int i=0; i<fact.size(); ++i){
	                    if(isVariable(erasePattern[i]) && mod==0){
	                        cout<<"["<<erasePattern[i]<<"="<<fact[i]<<"] ";
	                    }else if(mod!=1 || !isVariable(erasePattern[i])){
	                        cout<<fact[i]<<" ";
	                    }
	                }
	                cout<<"\b\n";
	            }
	        }
	        continue;
		}else if(t1=="ls"){
			for(auto &a:known){
				for(auto &b:a){
					cout<<b<<" ";
				}
				cout<<"\b;\n";
			}
			cout<<".\n";
			continue;
		}else if(t1=="mode"){
			ss>>t1;
			if(t1=="vars"){
				mod=0;
			}else if(t1=="plain"){
				mod=2;
			}else if(t1=="full"){
				mod=1;
			}else{
				cout<<"Failed.\n";
				continue;
			}
			cout<<"Ok.\n";
			continue;
		}
		while(ss>>t1){
			if(t1=="by")ir=1;
		}
		if(ir){
			
		}else{
			stringstream ss(in);
			vector<string> vs;
			while(ss>>t1){
				thing.insert(t1);
				vs.push_back(t1);
			}
			known.insert(vs);
			cout<<"Ok.\n";
		}
	}
    //凑够200行
}